Nuprl Lemma : void-list-equality
0,22
postcript
pdf
x
,
y
:Void List.
x
~
y
latex
Definitions
t
T
,
Void
,
type
List
,
x
:
A
B
(
x
)
,
s
~
t
,
x
:
A
.
B
(
x
)
origin
x, y:Void List. x ~ y x, y:Void List. x ~ y 
T
B(x)x:A. B(x)